x, y:. (x z y)  (x  y) 

latex

Up	bool 1, bool 1
Definitions	t  T, A  B, i z j, x:A. B(x), P & Q, P  Q, P  Q, P  Q,
Lemmas	assert of bnot, iff functionality wrt iff, not wf, lt int wf, bnot wf, assert wf, assert of lt int, not functionality wrt iff